(* $Id: PFOLEncodedEnv.ml 117 2007-10-21 17:27:07Z yann.regisgianas $ *)

(* Pangolin, a functional programming language for correct programs.
   Copyright (C) 2007, Yann Régis-Gianas, François Pottier.
   Contact: yann.regisgianas@gmail.com

   This program is free software: you can redistribute it and/or modify
   it under the terms of the GNU General Public License as published by
   the Free Software Foundation, either version 3 of the License, or
   any later version.

   This program is distributed in the hope that it will be useful,
   but WITHOUT ANY WARRANTY; without even the implied warranty of
   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
   GNU General Public License for more details.

   You should have received a copy of the GNU General Public License
   along with this program.  If not, see <http://www.gnu.org/licenses/>. *)

open PFOLSyntax
open PFOLSyntaxExt
module X = XCoreSyntax
open XCoreSyntaxExt
open XCoreLifting
open PFOLEnv
open PFOLTypesEncoding
open PFOLEncoding

type env = PFOLEnv.env

let introduce_rigid_type_variables = PFOLEnv.introduce_rigid_type_variables

let empty = PFOLEnv.empty

let bind_value pos env x fty = 
  let s = encode_xtype_scheme_as_type_scheme pos env fty in
    PFOLEnv.bind_value pos env x s

let bind_logic_value = PFOLEncoding.bind_logic_value

let bind_fact pos env f =
  let (env, f) = encode_formula_as_predicate pos env f in
    PFOLEnv.bind_fact pos env f

let bind_logic_function pos env f s =
  fst (bind_logic_value pos env f s)

let logic_clause_as_formula pos f ret_ty bs abs =
  let args = List.map (fun (x, _) -> X.FVar x) bs in
  let args_prod = mk_fprod pos args in
  let args_ty = X.FTProd (List.map (fun (_, ty) -> ty) bs) in
  let (p, body) = X.open_logic_clause_abs abs in
  let xbs, ts = pattern_as_bindings p in
    XCoreSyntaxExt.mk_conj pos
      (mk_fforalltys pos ts 
	 (mk_lforall pos bs 
	    (mk_lforall pos (to_logic_bindings xbs)
	       (mk_fimply pos 
 		  (mk_feq pos args_ty args_prod (pattern_as_logic_value pos p))
		  (mk_feq pos ret_ty (mk_fapp pos (X.FVar f) args) body.X.fvalue))
	    )))
      (mk_fforalltys pos ts 
	 (mk_lforall pos (to_logic_bindings xbs)
	    (mk_feq pos ret_ty 
	       (mk_fapp pos (X.FVar f) [pattern_as_logic_value pos p])
	       body.X.fvalue)))


let bind_logic_function_definition pos env f s def = 
  let env, a = bind_logic_value pos env f s in
    match def with
      | X.LFInductive abs ->
	  let (vs', ids, lcs) = X.open_lfi_abs abs in
	  let (vs, bs, ret_ty) = 
	    destruct_formula_type_scheme_as_poly_bindings pos s ~ids 
	  in
	    List.fold_left 
	      (fun env lc ->
		 bind_fact pos env 
		   (mk_lformula pos 
		      ((mk_fforalltys pos (vs @ vs')
			  (logic_clause_as_formula pos f ret_ty bs lc)))))
	      env lcs

      | X.LFAbbrev d when is_deferred_formula d ->
	  env

(* Predicate binding. *)

let bind_predicate pos env p s def =
  let s = encode_formula_type_scheme_as_object_type_scheme pos env s in
  let (env, a, b) = PFOLEnv.bind_predicate pos env p s def in
  let object_def = 
    let (vs, bs, xs, ret_ty) = destruct_type_scheme pos s in
      ForallTys 
	(create_polyf_abs 
	   (vs, 
	    Forall 
	      (create_forall_abs 
		 (bs, [], LogicBinOpApp 
		    (Equiv,
		     PApp (b, xs),
		     Reify (PredObjectApp (Var a, xs)))))))
  in
  let env = PFOLEnv.bind_fact pos env object_def in 
    env 

(** [bind_predicate_type_scheme pos env p s] introduces two atoms in
    PFOL.  The first one is a predicate whose type scheme is the
    encoding of [s].  The second one is an object whose type scheme is
    the object encoding of [s]. *)
let bind_predicate_type_scheme pos env p s = 
  let es = encode_formula_type_scheme_as_predicate_type_scheme pos env s in
    bind_predicate pos env p s (PredDec es)

(** [bind_predicate_defintion] encodes a PHOL predicate definition in PFOL. 

    - Abbreviations are encoded using propositional equivalence. 
    - Inductive definitions are axiomatized. *)
let bind_predicate_definition pos env p s pdef =
  match pdef with
    | X.PDAbbrev f when is_deferred_formula f ->
	bind_predicate_type_scheme pos env p s

    | X.PDAbbrev f ->
	(* f has the form: [forall ts. fun bs -> t]. We extract 
	   [ts], [bs] and bind them in the environment. *)
	let (vs, ins, t) = destruct_poly_flam f.X.fvalue in
	let tvs = List.map (fun v -> (v, X.KStar)) vs in
	let env = introduce_rigid_type_variables pos env tvs in
	let (env, locals), bs = 
	  encode_bindings pos (env, Var.AtomSet.empty) ins 
	in
	  (* We encode [t]. *)
	let env, t = 
	  encode_formula_as_predicate pos env (mk_lformula pos t) 
	in
	  remove_locals locals 
	    (bind_predicate pos env p s
	       (PredDef 
		  (create_predicate_def_abs 
		     (type_parameters env vs, 
		      bs, 
		      t))))

    | X.PDInductive cases ->
	let env = bind_predicate_type_scheme pos env p s in
	let env = List.fold_left (bind_fact pos) env cases in
	  bind_fact pos env (inductive_inversion pos p s cases)

let bind_dataconstructor pos ts env (d, ex_ts, ty) = 
  let s = mk_formula_type_scheme (ts @ ex_ts) (inject_term_type ty) in
  let env = fst (bind_logic_value pos env d s) in
    bind_fact pos env (mk_lformula pos (injective_dataconstructor pos d s))

let bind_type_definition pos env t k def = 
  let env = introduce_rigid_type_variable pos env (t, k) in
    match def with
      | X.DAlgebraic (ts, ds) ->
	  let env = List.fold_left (bind_dataconstructor pos ts) env ds in
	  let ds = 
	    List.map (fun (d, ex_ts, ty) -> (d, ex_ts, lift_term_type ty)) ds 
	  in
	    bind_fact pos env 
	      (mk_lformula pos (complete_dataconstructors pos t ts ds))

      | X.DeferredType ->
	  env

